i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), a:((k:{k:Knd| 
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), a:((k:{(k  ks)} 
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), a:((decl-state(ds)
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), a:((ma-valtype(da;
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), a:((ma-valtype(k)
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), a:((T)),
upd:update-spec(ds; da).
((fpf-dom(id-deq; x; ds)))
 update-spec-decl(upd; ds)
 (ecl-machine2(i; ds; da; x; T; ks; a; upd)  es_realizer{i:l}) 

latex

Definitions

fpf-ap(f; eq; x), fpf-join(eq; f; g), fpf-single(x; v), Type, fpf-compatible(A; a.B(a); eq; f; g), x:AB(x), x:A. B(x), s = t, t  T, strong-subtype(A; B), P  Q, x. t(x), fpf(A; a.B(a)), type List, update-spec(ds; da), A, update-spec-decl(upd; ds), (x  l), [], <a, b>, Kind-deq, Knd, product-deq(A; B; a; b), fpf-cap(f; eq; x; z), f(a), if b then t else f fi , let x,y = A in B(x;y), list_accum(x,a.f(x;a); y; l), {x:A| B(x)} , x:A  B(x), x,y. t(x;y), decl-state(ds), ma-valtype(da; k), prop{i:l}, x.A(x), R-state-var(i; ds; da; x; T; ks; tr), atom{$n:n}, a < b, x:A. B(x), es_realizer{i:l}, update-spec-vars(upd), Rall(L; x.R(x)), ecl-machine2(i; ds; da; x; T; ks; a; upd), , , top, id-deq, fpf-dom(eq; x; f), b, Id, subtype(S; T), EqDecider(T), isect(A; x.B(x)), t.1, void, t.2, left + right, Unit, P  Q, P  Q, , A  B, b, False, case b of inl(x) => s(x) | inr(y) => t(y), guard(T), P  Q, sqequal(s; t), ff, eq_bool(p; q), i <z j, i z j, (i = j), eq_atom(x; y), null(as), set_blt(p; a; b), x f y, grp_blt(g; a; b), dcdr-to-bool(d), eq_atom{$n:n}(x; y), q_le(r; s), q_less(a; b), qeq(r; s), eq_lnk(a; b), eq_id(a; b), deq-member(eq; x; L), bimplies(p; q), band(p; q), bor(p; q), tt

Lemmas

fpf-join-ap-sq, fpf-compatible-single-iff, bnot wf, subtype rel self, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf-single wf, fpf-cap-join-subtype, fpf-cap wf, subtype rel dep function, pi2 wf, pi1 wf, eqof eq btrue, fpf-cap-single, fpf-join-cap-sq, ifthenelse wf, Kind-deq wf, product-deq wf, list accum wf, update-spec-decl wf, not wf, assert wf, fpf-dom wf, top wf, subtype rel wf, fpf-trivial-subtype-top, update-spec wf, nat wf, bool wf, fpf wf, Rall wf, update-spec-vars wf, es realizer wf, R-state-var wf, fpf-single wf3, ma-valtype wf, id-deq wf, fpf-join wf, decl-state wf, member wf, l member wf, Knd wf, fpf-ap wf, Id wf, fpf-compatible wf